효과적인 멀티태스크 프로그램 검증을 위한 KLEE와 CBMC의 오경보 식별 성능 비교

김동우; 최윤자; Dongwoo Kim; Yunja Choi

연구문헌

국내 논문지

홈 > 연구문헌 > 국내 논문지 > 한국정보과학회 논문지 > 정보과학회논문지 (Journal of KIISE)

정보과학회논문지 (Journal of KIISE)

Current Result Document : 8 / 351 이전건 다음건

한글제목(Korean Title)	효과적인 멀티태스크 프로그램 검증을 위한 KLEE와 CBMC의 오경보 식별 성능 비교
영문제목(English Title)	Comparison of False Alarm Detection using KLEE and CBMC for Effective Multitask Program Verification
저자(Author)	김동우 최윤자 Dongwoo Kim Yunja Choi
원문수록처(Citation)	VOL 48 NO. 02 PP. 0174 ~ 0182 (2021. 02)
한글내용 (Korean Abstract)	OiL-CEGAR[1]는 정확한 검증을 위해 정형 운영체제 모델을 사용하고 프로그램을 정형모델로 변환해 검증함으로써 운영체제와 프로그램 모두를 고려하여 검증하였다. 하지만, 프로그램의 추상화로 인한 오경보가 보고될 수 있었으며 이를 제거하기 위한 실행 가능성 검사는 고비용이 요구되어 검증 성능 개선을 위해서는 오경보 식별 성능의 개선이 꼭 필요하다. 본 연구에서는 실행 가능성 검사를 위한 두 가지 방법을 소개하고 비교하였다. 첫 번째 방법은 CBMC를 이용하며 전체 프로그램의 수식을 만들고 반례에 나타난 모든 블록의 도달 가능성을 한 번에 확인한다. 두 번째 방법은 KLEE를 이용하며 이진 탐색 기반 실행 가능성 검사를 통해 반례의 실행 불가능한 블록을 식별한다. 실험에서는 차량전장용 창문 제어프로그램의 검증에 각 실행 가능성 검사를 적용한 결과 KLEE를 이용했을 때 실행 가능성 검사 시간을 1/2000 수준으로 낮추었으며 전체 검증 시간을 11.78% 단축할 수 있었다.
영문내용 (English Abstract)	OiL-CEGAR[1] verifies the composition of a formal OS model and an abstracted application program for accurate verification. Due to the use of the abstract program, however falsealarms can be reported and executability checking for identifying false-alarms requires a high cost. Therefore, efficient executability checking is essential to improve verification performance. To find an effective executability checking method, this study introduces and compares two different techniques that perform executability checking. The first one collects the Boolean formula for the entire program and checks the reachability of all the program blocks in the counterexample by using CBMC. While the second one uses KLEE and identifies non-executable blocks in the counterexample through the binary search-based executability checking. The suggested executability checking methods are applied to a window controller program from the automotive domain. Results show that executability checking using KLEE takes only 1/2000 time compared to that of CBMC and reduces 11.78% of OiL-CEGAR verification costs.
키워드(Keyword)	멀티태스크 프로그램 검증 OiL-CEGAR KLEE CBMC multitask program verification
파일첨부	PDF 다운로드